COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	| CALIBAN'S WILL by M. H. Newman.  When Caliban's will was opened
C00005 ENDMK
C⊗;
COMMENT | CALIBAN'S WILL by M. H. Newman.  When Caliban's will was opened
it was found to contain the following clause:

	"I leave ten of my books to each of Low, Y.Y. and 'Critic', who
are to choose in a certain order.

	"No person who has seen me in a green tie is to choose before Low.

	"If Y.Y. was not in Oxford in 1920 the first chooser never lent me
a green umbrella.

	If Y.Y. or 'Critic' has second choice, 'Critic' comes before the
one who first fell in love."

	Unfortunately, Low, Y.Y. and "Critic" could not remember any of
the relevant facts, but the family solicitor pointed out that, assuming
the problem to be properly constructed (i.e. assuming it to contain no
statement superfluous to its solution), the relevant data and order could
be inferred.

	What was the prescribed order of choosing, and who lent Caliban
an umbrella? -- from Caliban's Problem Book - Dover 1961 |

declare INDCONST Low YY Critic Firstfell First Second Third ε Person;
declare INDVAR s so s1 s2 ε Person;
declare PREDCONST sgt(Person) ninox(Person) nlu(Person);
declare PREDCONST precedes(Person,Person) [inf];

axiom person:	∀s.(s=Low ∨ s=YY ∨ s= Critic)
		∀s.(s=First ∨ s=Second ∨ s=Third)
		¬(Low=YY) ∧ ¬(Low=Critic) ∧ ¬(YY=Critic)
;;

axiom a:	∀s.(sgt(s) ⊃ ¬(s precedes Low));;

axiom b:	ninox(YY) ⊃ nlu(First);;

axiom c:	Second=YY ∨ Second=Critic ⊃ Critic precedes Firstfell;;